COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input macro[1,mps]
C00015 ENDMK
C⊗;
\input macro[1,mps]
\magnification\magstephalf
\baselineskip 14pt
\leftline{\sevenrm A83.Tex[254,mps]\today}
\leftline{\copyright\sevenrm Robert W. Floyd, December 12, 1988}
\leftline{\sevenrm Unpublished draft}
\def \fhat{{\hat f}}
\def \fhafhat{{\skew 8\hat\fhat}}
\bigskip
\noindent {\bf Least Fixed Points}

Languages and other sets are frequently defined by formulas that are
equations $X=f(X)$ or inclusions $X\supseteq f(X)$, where $f$ is a
monotone function.  Often, as in $X = X \cup XX$, there is more than
one solution.  (Solutions of the example include $\emptyset, \Lambda, \hbox {and} 
\, a↑*.)$  We shall show that there is always a unique least solution, a
subset of all the others.  It is customary to regard an equation or inclusion
as defining the language that is its least solution.  We start by proving
theorems about set formulas in general.  These fixed point theorems are
useful elsewhere in computer science, particularly in recursive function theory.

Let $\bf U$ be an arbitrary domain.  Let $f$ be a monotone function on 
$2↑{\bf U}$.
Define 
$${\cal C} = \{X\mid X \supseteq f(X)\},$$ 
the class of  sets contracted
by $f$.  ${\cal C}$ is nonempty, because $\bf{U}\supseteq f(\bf{U})$.  
If $Y\in {\cal C}$, $Y \supseteq f(Y)$, $f(Y) \supseteq f(f(Y))$, so
$Y\in {\cal C}$ implies $f(Y) \in {\cal C}$.  Define 
$$L = \bigcap {\cal C}.$$
If $Y\in{\cal C}$, $L=\bigcap{\cal C} = Y \cap
\bigcap {\cal C} \subseteq Y$, $f(L) \subseteq f(Y)
\subseteq Y$, so $f(L) \subseteq \bigcap {\cal C} = L$, $L\in {\cal C}$.
That is, $L$ is the least member of ${\cal C}$.  Then $f(L) \in {\cal C}$, 
$L \subseteq f(L)$, so $L = f(L)$; $L$ is a solution of $X = f(X)$.  Since
any solution of $X = f(X)$ is a solution of $X \supseteq f(X)$, $L$ is the
unique least solution of $X = f(X)$, also known as the least fixed point
(LFP) of $f$.

Define $\fhat$ by $\fhat(X) = \widetilde{f({\tilde X})}$.  This is a dual 
relation between functions:
$\fhafhat (x) = \widetilde{\hat{f}({\tilde x})} = \widetilde{\widetilde{f(\tilde
{\tilde x})}} = f(x)$.  If $f$ is monotone and
$X\subseteq Y$, then ${\tilde Y}\subseteq {\tilde X}$, $f({\tilde Y})\subseteq
f({\tilde X})$, $\widetilde {f({\tilde X})}$ $\subseteq \widetilde 
{f({\tilde Y})}$, so $\fhat$ is also monotone.

If $X \supseteq f(X)$, $\fhat ({\tilde X}) = \widetilde {f(X)} 
\supseteq \tilde X$, and conversely $Y \subseteq \fhat (Y)$ implies
$\tilde Y \supseteq f({\tilde Y})$.  Also, $X = f(X)$ implies ${\tilde X} =
\fhat ({\tilde X})$, $Y = \fhat (Y)$ implies ${\tilde Y} = f({\tilde Y})$.  Since
we know $\fhat$ has a LFP $\hat L$, $\tilde{\hat L}$ is a fixed
point of $f$ that includes every fixed point, i.e., the greatest fixed point
(GFP) of $f$; since $L$ is the intersection of all solutions of
$X\supseteq \fhat (X)$, $\tilde{\hat L}$ is the union of all solutions
of $X \subseteq f(X)$.

(There is also a direct proof of the existence of a GFP of $f$, dual to the
proof of existence of a LFP. Drill:  Find this proof.)

If we have several (say, two) simultaneous inclusions on set-valued variables
$$\left.\eqalign{X↓1&\supseteq f↓1(X↓1, X↓2\cr
X↓2 &\supseteq f↓2(X↓1, X↓2)\cr}\right\}\eqno(*)$$
we shall show that there is a pair of sets $X↓1 = L↓1$, $X↓2 = L↓2$ that
satisfies the inclusion, is less than any other solution, and satisfies
the corresponding equalities.  Define $\Pi(X↓1, X↓2) = (\{1\} \times  X↓1)
\cup (\{2\} \times X↓2)$; that is, if $X↓1 = \{\hbox {A, B, C}\}$ and
$X↓2 = \{\hbox{B, D}\}$, $\Pi (X↓1, X↓2) = \{\langle 1, \hbox {A}\rangle,
\langle 1, \hbox {B}\rangle, \langle 1, \hbox {C}\rangle, \langle 2, \hbox {B}
\rangle, \allowbreak \langle 2, \hbox {D}\rangle\}$.  There are obvious 
inverse functions
$\alpha$ and $\beta$ that recover $X↓1$ and $X↓2$ from $\Pi(X↓1, X↓2)$;
all three functions are monotone.  (The range of $\Pi$ and the domain 
of $\alpha, \beta$ are the subsets of $\{1, 2\} \times U.)$  Drill: 
Define $\alpha$ and $\beta$.
\medskip
\noindent{\bf Answer:}  $\alpha$ is the set extension of the function that maps
$\langle1,x\rangle$ to $x$.
\medskip
Now we convert the simultaneous inclusions into a single incluson:
$$\eqalign{Z\supseteq \Pi(f↓1(\alpha(Z), \beta(Z)), f↓2(\alpha(Z),
\beta(Z))) = g(Z)}\eqno(**)$$
Simple manipulation shows that if $Z$ satisfies ($**$), letting $X↓1 = \alpha(Z),
X↓2 = \beta(Z)$ satisfies ($*$); conversely, if $\langle X↓1, X↓2\rangle$ satisfies
($*$), letting $Z = \Pi(X↓1, X↓2)$ satisfies ($**$).  We conclude that if 
$f↓1$ and
$f↓2$ are monotone, $g$ is monotone, there is a LFP $\Pi(L↓1, L↓2)$ of $(g)$,
which gives a least solution $X↓1 = L↓1, X↓2 = L↓2$ of ($*$), with equality.
If $M↓1, M↓2$ is any other solution of ($*$), $L↓1 \subseteq M↓1, L↓2
\subseteq M↓2$.  Similarly, sets of simultaneous formulas have a greatest
fixed point; all the results obtained for single formulas go over to 
simultaneous ones.  (A direct proof is possible, but would be cluttered.)

Take a set of simultaneous equations
$$\left.\eqalign{X & \supseteq f(X,Y,g(X,Y))\cr
Y&\supseteq h(X,Y)\cr}\right\}\rm\eqno(A)$$
\noindent and the set
$$\left.\eqalign{X & \supseteq f(X,Y,Z)\cr
Y & \supseteq h(X,Y)\cr
Z & \supseteq g(X,Y)\cr}\right\}\rm\eqno(B)$$
Show if $\langle L↓X, L↓Y\rangle$ satisfies (A), then $\langle L↓X, L↓Y, L↓Z
= g(L↓X, L↓Y)\rangle$ satisfies (B).  Conversely, if $\langle L↓X, \allowbreak
L↓Y, L↓Z
\rangle$ satisfies (B), $\langle L↓X, L↓Y\rangle$ satisfies (A).
We can therefore, by introducing extra language variables, define a set
of languages by simultaneous inclusions where only one function symbol is
used in each defining equation.
\medskip
{\bf Example:} $E \supset a \cup E + E \rightarrow E \supset a
\cup X$, $X\supset YE,\, Y \supset E+$.
\medskip
\noindent Lemma:

If $X \supseteq Z\cup XY$, by the following induction $X\supseteq ZY↑i$

\item\item{$\bullet$}
$X\supseteq  Z = ZY↑0$

\item\item{$\bullet$}
If $X\supseteq ZY↑i, X\supseteq ZY↑iY = ZY↑{i+1}$
\medskip
\noindent Therefore, if $X\supseteq Z\cup XY,\, X\supseteq ZY↑*;\, 
$if $X\supseteq \Lambda \cup XY,\, X \supseteq Y↑*;\, $if $X\supseteq Y\cup XY,\,  
X \supseteq Y↑+$

Take two sets of simultaneous inclusions, where $f$ is monotone:
$$\left.\eqalign{X & \supseteq Y↑{*}\cr
Y & \supseteq f(X,Y)\cr}\right\}\rm\eqno(A)$$
$$\left.\eqalign{X & \supseteq \Lambda \cup XY\cr
Y & \supseteq f(X,Y)\cr}\right\}\rm\eqno(B)$$

Let $\langle L↓X, L↓Y\rangle$ be the least solution of (A).  Then it
satisfies (A) with equality.  Because it satisfies (A.1) with equality,
and $Y↑{*} = \Lambda \cup XY$, it satisfies (B) with equality.  Any solution
of (B) has been shown to be a solution of (A) (possibly not with equality),
so if $\langle M↓Y, M↓Y\rangle$ were a solution of (B) and not a superset
of $\langle L↓X, L↓Y\rangle$, the latter would not be the least solution
of (A), absurd.  We conclude that (A) and (B) have the same least solution.  This
illustrates that any language definable by simultaneous regular formulas,
can be defined without using the star.  (Drill:  Give examples where (B) 
has solutions with equality not satisfying (A) with equality.)

For monotone $g$ and for each $Y$, the incluson $X \supseteq g(X,Y)$ has a
least value of $X$.  Call this $h(Y)$; $h(Y) = g(h(Y),Y)$.  (Drill:  
Show $h$ monotone.)

Take the two simultaneous systems
$$\left.\eqalign {X & \supseteq h(Y)\cr
Y & \supseteq f(X,Y)\cr}\right\}\rm\eqno(A)$$
$$\left.\eqalign{X & \supseteq g(X,Y)\cr
Y & \supseteq f(X,Y)\cr}\right\}\rm\eqno(B)$$
Let $\langle L↓X, L↓Y\rangle$ be the least solution of (A).  Then $L↓X = h(L↓Y)$
and $L↓Y \supseteq f(L↓X, L↓Y)$.  Because $L↓X = h(L↓Y) = g(h(L↓Y), L↓Y)
= g(L↓X, L↓Y)$, $\langle L↓X, L↓Y\rangle$ satisfies (B) with
equality.  Any solution of B has been shown (Lemma) to be a solution of A
(possibly not with equality), so if $\langle M↓X, M↓Y\rangle$ solved (B),
$L↓X \not\subseteq M↓X$ or $L↓Y \not\subseteq M↓Y$,
$\langle L↓X, L↓Y\rangle$ would not be a LFP of (A), contrary to
hypothesis.  We conclude:  (A) and (B) have the same least solution.
\bye